\section{Passivation In Other Languages}

We consider synchronous languages with sum (choice).

\paragraph{$CCS!$ without restriction}
Everything is decidable.

\paragraph{$CCS!$ without restriction plus passivation}

\[
 \frac{P \xrightarrow{~\alpha~} P'}{\pass{a}{P}  \xrightarrow{~\alpha~} \pass{a}{P'}} ~~\textsc{Loc}
\qquad 
 \pass{a}{P} \arr{~\outC{a}~}  \nil ~~\textsc{Pas}
\]

We require that the registers are initialized with zero, and if the Minsky machine terminates then the value of the registers is set to zero. 

Encoding of Minsky machines:

\begin{tabular}{l}   
\(  
\mathrm{\textsc{Register}}~r_j \qquad
\encp{r_j = m}{\mms}  =  \pass{r_j}{!inc_j.\outC{u_j} \parallel \prod_{1}^{m}\overline{u_j}}  \parallel \prod_{1}^{m}\overline{loop}
\) \\ \\
\(   
\begin{array}{lll}   
\multicolumn{3}{l}{\mathrm{\textsc{Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(r_j))}{\mms}&  = &  !p_i.\outC{inc_j}.(\outC{loop} \parallel \outC{p_{i+1}})\\  
\encp{(i: \mathtt{DECJ}(r_j,s))}{\mms}&  = & !p_i.(\outC{loop} \parallel u_j.loop.\outC{p_{i+1}}) \parallel \\
& & !p_i.r_j.(\pass{r_j}{!inc_j.\outC{u_j}} \parallel \outC{p_s}) 
\end{array}   
\) 
\end{tabular}

In parallel there is a process $loop.DIV$.


\begin{myrem} Some issues:
 \begin{itemize}
  \item Encoding of nested replication (one level)
  \item Encoding of sum (with passivation)
 \end{itemize}
\end{myrem}

Divergence is decidable (well-quasi order as in ICTAC paper with passivation). Convergence is undecidable.

\paragraph{\hof}
See ICTAC paper.

\paragraph{\hof plus passivation}

Encoding of Minsky machines:

\begin{tabular}{l}   
\(  
\mathrm{\textsc{Register}}~r_k \qquad
\encp{r_k = m}{\mms}   =  \pass{r_k}{\encn{m}{k}} 
\) \\ %where

\quad where \\
\(
\begin{array}{l}
 \qquad \encn{0}{k}  =  z_k \quad \quad   
\encn{n}{k}  =  u_k.\encn{n-1}{k} \\
\end{array}

\)\\  \\

\(
\begin{array}{lll}   
\multicolumn{3}{l}{\mathrm{\textsc{Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(r_k))}{\mms}&  = &  !p_i.( r_k(x).(\Ho{c_k}{x} \parallel \pass{r_k}{c_k(y).u_k.y} \parallel  \overline{p_{i+1}}))\\
\encp{(i: \mathtt{DECJ}(r_k,s))}{\mms}&  = & !p_i.(\overline{u_k}.\overline{p_{i+1}} + \overline{z_k}.r_k(x).(\pass{r_k}{z_k}\parallel \overline{p_s}))  
\end{array}   
\) 
\end{tabular}

Deterministic encoding; everything is undecidable.

\paragraph{\hocore vs. \hocore plus passivation}
\begin{itemize}
 \item Ideas with Alan (separation based on properties of encodings)
 \item Leader election (solvable with passivation, not solvable in \hocore)
\end{itemize}

